\subsection{Decidability of Bounded Adaptation}\label{sec:decwsts}
\input{terminationrecursion}
\input{predbasis}


\subsection{Undecidability of Eventual Adaptation} \label{sec:unde2d}
Here we show that  \LG  is undecidable in \evols{2} by relating it to termination  in \mmss;
this result carries over to \evols{1}, \evold{1},  and \evold{2}---see Corollary \ref{cor:ba-undec}.
This relationship is obtained by defining an encoding tailored to the features of the property.
In contrast to the encoding given in Section \ref{s:ev1}, 
the encoding presented here is \emph{non faithful} as it may 
perform erroneous tests for zero on the registers (i.e.
in the simulation of the \mm a register
is assumed to contain the value zero even if this is not the case). Nevertheless, we are able to define encodings that repeatedly simulate finite computations of the \mm, and if the number of repeated simulations is infinite, then we have the guarantee that the number of erroneous steps is finite. Thus infinitely
many of the performed simulations are correct.
This way, the \mm terminates iff its encoding has a non terminating computation. As during its execution the encoding continuously exhibits a barb on $e$, 
it %then follows that \LG is undecidable in \evol{-}.
then follows that \LG is undecidable for \evols{2} processes.


The encoding relies on finitely many output prefixes acting as \emph{resources} on which instructions of the \mm depend in order to be executed.
To repeatedly simulate finite runs of the \mm,
at the beginning of the simulation
the encoding produces finitely many instances of these resources. % needed to simulate every \mm step.
When $\mathtt{HALT}$ is reached, 
the registers are reset, some of the consumed resources 
are restored, and a new simulation is restarted from the  first instruction.
In order to guarantee that an infinite computation
of the encoding %of the \mm 
contains only finitely many
erroneous jumps, 
finitely many instances of 
a second kind of
resource (different from that required to execute instructions) 
are produced. 
Such a resource is consumed 
by increment instructions and restored by 
decrement instructions.
When the simulation performs a jump, the tested register is reset: 
if it was not empty (i.e., an erroneous test) then some resources are permanently lost. 
When 
the encoding runs out of 
resources, the simulation will
eventually block as increment instructions can no longer be simulated.
We make two non restrictive assumptions. First, we assume that a
\mm computation contains at least one increment instruction.
Second, in order to avoid resource loss at the end
of a correct simulation run, we
 assume that \mm computations terminate
with both the registers empty.

\begin{table}[t]
 \linefigure\\
\quad \\

 \begin{tabular}{l} 
$\controll ~= ~!a.(\outC{f} \parallel \outC{b} \parallel  \outC{a}) \parallel \outC{a}.a.(\outC{p_1} \parallel e) \parallel \
!h.(g.\outC{f} \parallel \outC{h})$
  \\
$\mathrm{\textsc{Register}}~r_j $ \\
\ \  \(  
\encp{r_j = m}{\mmn{2}}=\left\{  
\begin{array}{ll}  
 \component{r_j}{!inc_j.\outC{u_j} \parallel \outC{z_j}}  & \textrm{if } m= 0 \\  
 \component{r_j}{!inc_j.\outC{u_j} \parallel \prod^{m}\overline{u_j} \parallel \outC{z_j} }  
%\parallel \prod_{1}^{m}\overline{w} 
~~& \textrm{if } m> 0 .  
\end{array}\right.  
\) \\ 
\(   
\begin{array}{ll}   
\multicolumn{2}{l}{\mathrm{\textsc{\!\!Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mmn{2}}&  =   !p_i.f.(\outC{g} \parallel b.\outC{inc_j}.
%(\outC{w} \parallel 
\outC{p_{i+1}})\\  
\encp{(i: \mathtt{DECJ}(r_j,s))}{\mmn{2}} \! \! \! \! \!&  =  !p_i.f.\big(\outC{g} \parallel (u_j.(\outC{b} \parallel
           \outC{p_{i+1}}) \\
& \qquad +   z_j.\update{r_j}{\component{r_j}{!inc_j.\outC{u_j} \parallel \outC{z_j}}}. \outC{p_s})\big) \\
\encp{(i: \mathtt{HALT})}{\mmn{2}}&  =  !p_i.%.w.
                  \outC{h}.h.\update{r_0}{\component{r_0}{!inc_0.\outC{u_0} \parallel \outC{z_0}}}.\update{r_1}{\component{r_1}{!inc_1.\outC{u_1} \parallel \outC{z_1}}}.\outC{p_1}
\end{array}   
\) 
\end{tabular}
\caption{Encoding of \mmss into $\evols{2}$} \label{tab:minskyccsbs}
 \linefigure
\end{table}



We now discuss the encoding defined in 
Table~\ref{tab:minskyccsbs}. 
We first comment on \controll, 
the process that manages  the resources.
It is composed of three processes in parallel.
The first replicated process is able  
to produce an unbounded amount of processes $\outC{f}$ and 
$\outC{b}$, which represent the two kinds of resources
described above. The second process starts and stops
a resource production phase by performing $\outC{a}$
and $a$, respectively. Then, it starts the \mm simulation
by emitting the program counter $\outC{p_{1}}$.
The third process is used at the end of the simulation
to restore some of the consumed resources $\outC{f}$
(that are transformed in $\outC{g}$, see below).

A register $r_j$ that stores number $m$ is encoded as 
%a component that
an adaptable process at $r_{j}$ containing 
$m$ copies of the unit process $\outC{u_j}$. 
It also contains process $!inc_j.\outC{u_j}$ which allows to create further copies of $\outC{u_j}$
when an increment instruction is executed. 
Instructions are encoded as replicated processes guarded by $p_i$.
Once $p_i$ is consumed, 
increment and decrement instructions
%in order to execute the corresponding instruction it is necessary to 
consume one of the resources 
$\outC{f}$. If such a resource is available then it is renamed as
$\outC{g}$, otherwise the simulation blocks.
The simulation of an increment instruction also consumes an instance of resource $\outC{b}$.

The encoding of a decrement-and-jump instruction is 
slightly more involved.
It is implemented as a choice:  
the process can either perform a decrement and proceed 
with the next instruction, or to jump.
In case the decrement can be executed (the input $u_{j}$
is performed) then a resource $\outC{b}$ is restored.
%As discussed above, t
The jump branch can be taken even if the register is not
empty. In this case, the register is reset via an
update that restores the initial state of the adaptable process at $r_{j}$.
Note that if the register was not empty, then some processes $\outC{u_{j}}$ are lost.
Crucially, this causes a permanent loss of a corresponding amount of resources $\outC{b}$, 
as these are only restored when process $\outC{u_{j}}$  
are consumed during the simulation of a decrement.

The simulation of the $\mathtt{HALT}$ instruction
performs two tasks before restarting 
the execution of the encoding  by reproducing the program counter $p_{1}$.
The first one is to restore some of the consumed
resources $\outC{f}$: this is achieved by  the third process of 
\controll, 
which 
repeatedly consumes one instance of $\outC{g}$
and produces one instance of $\outC{f}$. 
This process is started/stopped by executing the two prefixes $\outC{h}.h$.
The second task is to reset the registers by  
updating the adaptable processes at $r_{j}$ with their initial state.

The full definition of the encoding is as follows.

\begin{definition}\label{def:minskyconfs}
 Let $N$ be a \mm, with registers $r_0$, $r_1 $ and instructions
$(1:I_1) \ldots (n:I_n)$. 
Given the \controll process and the encodings in 
Table~\ref{tab:minskyccsbs}, the encoding of $N$ in \evols{2} (written $\encp{N}{\mmn{2}}$)
is defined as
$
\encp{r_0 = 0}{\mmn{2}} \parallel \encp{r_1 = 0}{\mmn{2}} \parallel \prod^{n}_{i=1} \encp{(i:I_i)}{\mmn{2}}  
 \parallel \controll$.
\end{definition}

As discussed above, the encoding has 
an infinite sequence of simulation runs if and only 
if the corresponding \mm terminates. As the barb $e$ is continuously
exposed during the computation (the process $e$ is spawn 
with the initial program counter and is never consumed), we can conclude
that a \mm terminates if and only if its encoding
does not eventually terminate the simulation runs. As
during the simulation runs the barb $e$ is always exhibited,
this coincides with checking whether the encoding
does not eventually adapt.
 




\begin{lemma} \label{th:corrE2}
 Let $N$ be a \mm. $N$ terminates iff $\encp{N}{\mmn{2}} \barbw{e}$.
\end{lemma}

\begin{proof}
See \ref{app:e2}.
\end{proof}

Exploiting  Lemma \ref{th:corrE2}
and proceeding exactly as the proof of
Theorem \ref{th.ev1} for \evols{1}, 
we can state the following.

\begin{theorem}\label{th:ev2}
\LG is undecidable in \evols{2}.
\end{theorem}
%\begin{proof}[Proof (Sketch)]
%Let $N$ be a \mma and and consider its encoding $\encp{N}{\mms}$. We have $\BC_{\encp{N}{\mms}}^{\emptyset}=\{\encp{N}{\mms}\}$.
%%consider the very simple cluster $C = \bullet$. 
%Undecidability of \LG  %$C[\encp{N}{\mms}]\negbarbk{\overline{e}}$ 
%follows from undecidability of the termination problem for Minsky machines
%and Lemma \ref{th:corrE2}. \qed
%%Then $C[\encp{N}{\mms}]\barbw{\overline{e}}$ immediately follows from Theorem \ref{th:corrE2}.
%%\end{proof}
%The proof 
%of Theorem \ref{th:ev2} 
%proceeds exactly as the proof of Theorem \ref{th.ev1} for \evols{1}.

Similarly as in that case, 
undecidability  extends also to \evold{2}, \evols{1} and \evold{1}. This easily follows from the fact that \evols{2} is a subcalculus of \evols{1} and from Lemma \ref{lem:statvsdyn}, since $\encp{N}{\mms}$ is a process in \evols{2} that does not contain any nested adaptable processes.
%\end{proof}

\begin{corollary}\label{cor:ba-undec}
\LG is undecidable in \evols{1}, \evold{1},  and \evold{2}.
\end{corollary}

Note that
the encoding $\encp{\cdot}{\mmn{2}}$ 
uses processes
that do not modify the topology 
of nested adaptable processes;  
update prefixes 
do not remove nor create adaptable processes:
they simply remove the processes currently in the updated 
locations and replace them with the predefined initial content.
One may wonder whether the ability to remove processes
is necessary for the undecidability result: 
%in the following, 
next 
we show that this is not the case.

